Nuprl Lemma : antecedent-surjection_wf
11,40
postcript
pdf
es
:ES,
P
,
Q
:(E
),
f
:({
e
:E|
P
(
e
)}
{
e
:E|
Q
(
e
)} ).
Q
f
P
latex
Definitions
x
:
A
.
B
(
x
)
,
,
t
T
,
Q
f
P
,
P
&
Q
,
x
:
A
.
B
(
x
)
Lemmas
antecedent-function
wf
,
es-E
wf
,
event
system
wf
origin
es:ES, P, Q:(E
), f:({e:E| P(e)} {e:E| Q(e)} ). Q 
f P 
es:ES, P, Q:(E), f:({e:E| P(e)} {e:E| Q(e)} ). Q f P x:A. B(x) T f P
x:A. B(x)